T:Type, a,x,y:T. l_before(x; y; cons(a; []); T)  False 

latex

Definitions	guard(T), True, P  Q, P  Q, P  Q, P  Q, P  Q, x:A. B(x), prop{i:l}, t  T, False
Lemmas	false wf, sublist wf, iff wf